Lemma contradiction_condition:
  forall A:Prop, A -> ~A -> False.
Proof.
  contradiction.
Qed.